/*
 * Alloy Analyzer
 * Copyright (c) 2002 Massachusetts Institute of Technology
 *
 * The Alloy Analyzer is free software; you can redistribute it and/or modify
 * it under the terms of the GNU General Public License as published by
 * the Free Software Foundation; either version 2 of the License, or
 * (at your option) any later version.
 *
 * The Alloy Analyzer is distributed in the hope that it will be useful,
 * but WITHOUT ANY WARRANTY; without even the implied warranty of
 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
 * GNU General Public License for more details.
 *
 * You should have received a copy of the GNU General Public License
 * along with the Alloy Analyzer; if not, write to the Free Software
 * Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA  02111-1307  USA
 */

package alloy.util;

import java.util.Iterator;
import java.util.Vector;

public class Queue {
    
    /**Overview : a generic queue of Objects 
     * Objects are inserted at the end or front of the queue, and are deleted from
     * the front of the queue. Queue is thread safe and mutable. 
     *
     * @specfiled elts \\ seq[object]
     */
    
    
    public String toString() {
	//effects : returns a String representation of this.
	
	String result = "";
	for (int i = 0; i<queue.size(); i++) {
	    result += queue.elementAt(i).toString();
	}
	return result;
    }
    
    private Vector queue;
    
    //CONSTRUCTORS
    
    /**
     * @requires : nothing
     * @effects : creates an empty Queue (this.elts = (empty sequence))
     */
    
    public Queue() {
	//effects : creates a new empty Queue
	
	queue = new Vector();
    }
    
    //MODIFIERS
    
    /**
     * @requires: obj != null
     * @modifies: this.elts
     * @effects: this.elts' = this.elts U obj
     */
    
    public synchronized void enqueueBack(Object obj) {
	//modifies : this
	//effects : appends <obj> to the end of the queue
	
	queue.addElement(obj);
    }
 
    /**
     * @requires: obj != null
     * @modifies: this.elts
     * @effects: this.elts' = obj U this.elts
     */
    
    public synchronized void enqueueFront(Object obj) {
	
	queue.add(0, obj);
    }
    
    /**
     * @requires: nothing
     * @modifies: this.elts
     * @effects: if this.elts == o U seq1
     *           then this.elts' = seq1
     *           else EmptyException
     */

    public synchronized Object dequeue() throws EmptyException {
	//modifies : this
	//effects : returns the first element of the queue after removing it
	//          from the queue. Unless the queue is empty
	//          =>EmptyException, no modification to this.
	
	Object result = null;
	try {
	    result = queue.remove(0);
	}catch(ArrayIndexOutOfBoundsException e) {
	    throw new EmptyException();
	}
	return result;
    }

    //OBSERVERS

    /**
     * @requires: nothing
     * @modifies: nothing
     * @returns: the number of elements in this.elts
     */
    public int size() {
	return queue.size();
    }

    /**
     * @requires: this not be modified while generator is in use
     * @modifies:  nothing
     * @effects: returns an Iterator over the elements in this.elts
     */

    public Iterator elements() {
	return new SafeIterator(queue);
    }

    /**
     * @requires: obj != null
     * @modifies: nothing
     * @effects: true if obj in this.elts
     */
    
    public boolean isQueued(Object obj) {
	return queue.contains(obj);
    }
    
    //PRODUCERS
    
    /**
     * @requires: nothing
     * @modifies: nothing
     * @returns: a new Queue q' s.t. for every o in this.elts, o in q'.elts
     */
    
    public Queue copy() {
	
	Queue result = new Queue();
	for(int i = 0; i<queue.size(); i ++) {
	    result.queue.add(i, queue.get(i));
	}
	return result;
    }
}









